Issue4784a.agda:6,20-21
Variable x is declared erased, so it cannot be used here
when checking that the expression x has type A
